package karpiel.boguchwal.wojciech.przemek

import karpiel.boguchwal.wojciech.przemek.Ast._
import org.scalatest.FunSuite

class TypeInfererTest extends FunSuite {

  test("z czytajmnie") {
    implicit val cache: Cache = RealCache()
    implicit val ctx: Context = Context.Empty
    assert(PiValue(Universe(0), PiValue(Bruijn(0), Bruijn(0))).inferType == PiType(Universe(0), PiType(Bruijn(0), Bruijn(1))))
    assert(PiElim(PiValue(Universe(0), PiValue(Bruijn(0), Bruijn(0))), UnitType).inferType == PiType(UnitType, UnitType))
    assert(PiElim(PiElim(PiValue(Universe(0), PiValue(Bruijn(0), Bruijn(0))), UnitType), UnitValue).inferType == UnitType)
  }

  test("testInferType") {
    implicit val cache: Cache = RealCache()
    implicit val ctx: Context = Context.Empty
    assert(PiValue(UnitType, Bruijn(0)).inferType(Context.Empty, implicitly) == PiType(UnitType, UnitType))
    assert(PiElim(PiValue(UnitType, Bruijn(0)), UnitValue).inferType(Context.Empty, implicitly) == UnitType)
    val polymorphicIdentity = PiValue(Universe(0), PiValue(Bruijn(0), Bruijn(0)))
    assert(polymorphicIdentity.inferType(Context.Empty, implicitly) == PiType(Universe(0), PiType(Bruijn(0), Bruijn(1))))
    assert(PiElim(polymorphicIdentity, UnitType).inferType(Context.Empty, implicitly) == PiType(UnitType, UnitType))

    val newCtx = Context.Empty.append(IdType(UnitValue, UnitValue))(implicitly)
    assert(polymorphicIdentity.inferType(newCtx, implicitly) == PiType(Universe(0), PiType(Bruijn(0), Bruijn(1))))
    assert(PiElim(polymorphicIdentity, UnitType).inferType(newCtx, implicitly) == PiType(UnitType, UnitType))
  }

  test("Sum") {
    implicit val cache = RealCache()
    implicit val ctx: Context = Context.Empty
    assert(SumInr(BoolType, UnitValue).inferType == SumType(BoolType, UnitType))
    assert(SumInl(BoolTrue, UnitType).inferType == SumType(BoolType, UnitType))
    assert(SumElim(PiValue(BoolType, BoolTrue), PiValue(UnitType, BoolFalse)).inferType == PiType(SumType(BoolType, UnitType), BoolType))
    assert(PiElim(SumElim(PiValue(BoolType, BoolTrue), PiValue(UnitType, BoolFalse)), SumInr(BoolType, UnitValue)).inferType == BoolType)
    assertThrows[TypecheckException](PiElim(SumElim(PiValue(BoolType, BoolTrue), PiValue(BoolType, BoolFalse)), SumInr(BoolType, UnitValue)).inferType)
  }

  test("bool") {
    implicit val cache = RealCache()
    implicit val ctx: Context = Context.Empty

    def neg = BoolElim(BoolFalse, BoolTrue)

    assert(neg.inferType == PiType(BoolType, BoolType))
    assert(BoolElim(UnitType, BoolType).inferType == PiType(BoolType, Universe(0)))
    assertThrows[Exception](BoolElim(UnitValue, BoolTrue).inferType)
  }
  test("sigma") {
    implicit val cache: Cache = RealCache()
    implicit val ctx: Context = Context.Empty
    val sigmaType = SigmaType(PiValue(BoolType, PiElim(BoolElim(UnitType, BoolType), Bruijn(0))))
    val sigmaValue = SigmaValue(BoolTrue, UnitValue, PiValue(BoolType, PiElim(BoolElim(UnitType, BoolType), Bruijn(0))))
    assert(sigmaValue.inferType == sigmaType)
    val ctx2 = Context.Empty.append(sigmaType)
    assert(Proj1(Bruijn(0)).inferType(ctx2, implicitly) == BoolType)

    def insertReturnType(retT: Ast) = PiType(sigmaType, retT)

    val f1 = SigmaElim(PiValue(BoolType, PiValue(PiElim(BoolElim(UnitType, BoolType), Bruijn(0)), UnitType)))
    assert(f1.inferType == insertReturnType(Universe(0)))
    val f3 = SigmaElim(PiValue(BoolType, PiValue(PiElim(BoolElim(UnitType, BoolType), Bruijn(0)), Bruijn(1))))
    assert(f3.inferType == insertReturnType(BoolType))
  }
  test("sigma-pr2") {
    implicit val cache: Cache = RealCache()
    implicit val ctx: Context = Context.Empty
    val sigmaType = SigmaType(PiValue(BoolType, PiElim(BoolElim(UnitType, BoolType), Bruijn(0))))
    val sigmaValue = SigmaValue(BoolTrue, UnitValue, PiValue(BoolType, PiElim(BoolElim(UnitType, BoolType), Bruijn(0))))
    val ctx2 = Context.Empty.append(sigmaType)
    assert(Proj2(Bruijn(0)).inferType(ctx2, implicitly) == PiElim(BoolElim(UnitType, BoolType), Proj1(Bruijn(0))))
    val f2 = SigmaElim(PiValue(BoolType, PiValue(PiElim(BoolElim(UnitType, BoolType), Bruijn(0)), Bruijn(0))))
    assert(f2.inferType == PiType(sigmaType, PiElim(BoolElim(UnitType, BoolType), Proj1(Bruijn(0)))))
  }

  test("ID") {
    implicit val cache: Cache = RealCache()
    implicit val ctx: Context = Context.Empty
    assert(J(PiValue(BoolType, PiValue(BoolType, PiValue(IdType(Bruijn(1), Bruijn(0)), UnitType))), PiValue(BoolType, UnitValue)).inferType ==
      PiType(BoolType, PiType(BoolType, PiType(IdType(Bruijn(1), Bruijn(0)), UnitType))))


    assertThrows[Exception](J(PiValue(BoolType, PiValue(UnitType, PiValue(IdType(Bruijn(1), Bruijn(0)), UnitType))), PiValue(BoolType, UnitValue)).inferType)
    assertThrows[Exception](J(PiValue(BoolType, PiValue(BoolType, PiValue(IdType(Bruijn(1), Bruijn(0)), UnitType))), PiValue(UnitType, UnitValue)).inferType)
    assertThrows[Exception](J(PiValue(BoolType, PiValue(BoolType, PiValue(IdType(Bruijn(1), Bruijn(0)), UnitType))), PiValue(BoolType, BoolTrue)).inferType)
  }

  test("ID2") {
    implicit val cache: Cache = RealCache()
    import StdLib.Nat._
    implicit val ctx: Context = Context.Empty
    val two = PiElim(succ, one)
    val four_1 = PiElim(succ, PiElim(succ, two))
    val four_2 = PiElim(double, two)

    assert(Refl(four_1).inferType.normalized == IdType(four_1, four_2).normalized)
    assert(Refl(four_1).inferType.normalized == IdType(four_2, four_1).normalized)
    assert(Refl(four_2).inferType.normalized == IdType(four_1, four_2).normalized)
    assert(Refl(four_2).inferType.normalized == IdType(four_2, four_1).normalized)

    assertThrows[Exception](IdType(UnitValue, four_1).inferType)
    assertThrows[Exception](Refl(four_1).inferType.assertEquals(IdType(two, two)))
  }


  test("Empty") {
    implicit val cache: Cache = RealCache()
    val inExistent = IdType(BoolTrue, BoolFalse)
    val e = EmptyElim(inExistent)
    assert(e.inferType(Context.Empty, implicitly) == PiType(EmptyType, inExistent))
    assert(PiElim(e, Bruijn(0)).inferType(Context.Empty.append(EmptyType), implicitly) == inExistent)
  }

  test("Bool rec") {
    implicit val cache: Cache = RealCache()
    implicit val ctx: Context = Context.Empty
    val fn = PiValue(BoolType, PiElim(BoolElim(SumType(UnitType, UnitType), UnitType), Bruijn(0)))
    assert(BoolRec(fn, SumInl(UnitValue, UnitType), UnitValue).inferType ==
      PiType(BoolType, PiElim(BoolElim(SumType(UnitType, UnitType), UnitType), Bruijn(0))))
    assertThrows[Exception](BoolRec(PiValue(UnitType, PiElim(BoolElim(SumType(UnitType, UnitType), UnitType), Bruijn(0))), SumInl(UnitValue, UnitType), UnitValue).inferType)
    assertThrows[Exception](BoolRec(fn, SumInl(UnitValue, UnitType), BoolTrue).inferType)
    assertThrows[Exception](
      BoolRec(PiValue(BoolType, PiElim(BoolElim(SumType(UnitType, UnitType), Universe(0)), Bruijn(0))),
        SumInl(UnitValue, UnitType), BoolType).inferType)
  }

  test("W") {
    import StdLib.Nat._
    implicit val cache: Cache = RealCache()

    assert(natType.inferType(Context.Empty, implicitly) == Universe(0))

    assert(zero.inferType(Context.Empty, implicitly) == natType)
    assert(one.inferType(Context.Empty, implicitly) == zero.inferType(Context.Empty, implicitly))
    assert(one != zero)
    assert(one == PiElim(succ, zero).normalized(Context.Empty, implicitly))
    assert(zero != PiElim(succ, zero).normalized(Context.Empty, implicitly))
    assert(PiElim(succ, one).normalized(Context.Empty, cache) == PiElim(succ, PiElim(succ, zero)).normalized(Context.Empty, implicitly))
    val something = SumType(BoolType, PiType(UnitType, UnitType))
    val ctx = Context.Empty.append(something)
    assert(PiElim(succ, one).normalized(ctx, implicitly) == PiElim(succ, PiElim(succ, zero)).normalized(ctx, implicitly))
  }

  test("w2") {
    import StdLib.Nat._
    implicit val cache: Cache = RealCache()
    assert(double.inferType(Context.Empty, implicitly) == PiType(natType, natType))
    assert(PiElim(StdLib.Nat.double, StdLib.Nat.zero).inferType(Context.Empty, implicitly) == StdLib.Nat.natType)
    assert(PiElim(StdLib.Nat.double, StdLib.Nat.one).inferType(Context.Empty, implicitly) == StdLib.Nat.natType)
  }
}
